

对于网络设备$d \in D$，令变量序列$\{x_r^i,...,x_r^{l_r}\}$为规则$r \in T_d$的match域前缀匹配形式，我们规定编码$0 \rightarrow \bar{x_r^i}, 1 \rightarrow x_r^i$，$l_r$为规则$r$的前缀长度，，因此我们定义目标函数如下：
% 对于一个设备$d$，令$l_{max}=\max_{r \in T_d}l_r$为规则中的最长前缀长度，我们希望$l_{max}$尽可能小，从而节省更多的TCAM~\cite{vishnoi2014effective}存储空间，
\begin{equation}
	\label{equ:dpg-goal}
	\min \sum_{r \in T_d, d \in D}l_r
\end{equation}

公式~\ref{equ:dpg-goal} 目标在于使所有的数据平面规则match域的前缀长度之和最小，与其对应的约束条件如下：

\textbf{数据平面配置有效性约束}。令$\Pi = \bigcup_{\rho \in \mathbb{R}}\rho.\pi$为数据平面需求中所有路径集合，对于每条路径$\pi \in \Pi$，数据平面存在路径$\pi$，令$r(port)$表示action为发往端口$port$的规则，令$l_{min} = \min_{port \in \pi}l_{r(port)}$，令$r.start = x_r \times 2^{N - l_r}$, $r.end = r.start + 2^{N-l_r}$：
\begin{equation}
	\forall port \in \pi: r(port).start \le label_\pi < r(port).end
	% \forall port \in \pi: x_{r(port)} \le label_\pi < x_{r(port)} + 2^{N-l_{r(port)}}
\end{equation}
\begin{equation}
	\forall port' \in Port_d: match(r(port'), label_\pi) \Rightarrow l_{r(port')} < l_{r(port)}
\end{equation}
% \begin{equation}
% 	\forall \pi \in \Pi: \bigwedge_{port \in \pi}\bigwedge_{i=0}^{l_{r(port)}}x_{r(port)}^i
% \end{equation}

\textbf{数据平面配置无冲突约束}。对于每个设备$d \in D$，其任意两条规则不能冲突：
\begin{equation}
	\forall r_i, r_j \in T_d: r_i.start \ge r_j.end \vee r_i.end \le r_j.start
\end{equation}
% \begin{equation}
% 	\forall r_i, r_j \in T_d: \neg (\bigwedge_{i=0}^{l_{r_i}}x_{r_i}^i \wedge \bigwedge_{i=0}^{l_{r_j}}x_{r_j}^i)
% \end{equation}

最优性目标+有效性约束。

计算出最优的数据路径布局并为这些数据路径生成紧凑的规则可能会非常复杂。我们介绍了一种通用的方法来实现网络范围的策略，然后将过程建模为SAT问题，从而为交换机推导出路径和转发规则的最优编码。最后，在真实的ISP拓扑结构上进行评估，结果表明我们的解决方案与现有技术相比平均可以减少约50％的路径编码长度。

我们将网络描述为有向图 $G={V, A}$，其中每个顶点 $v \in V$ 表示拓扑中的一个节点，每条弧 $a=(src, dst)$，其中 $src, dst \in A$，表示可能的一跳数据包传输。需要对一组流路径 $P$ 进行编码，每条路径 $p \in P$ 是 $A$ 中一系列弧的序列，穿过一组节点 $N_p = \bigcup_{a \in p}{a.src, a.dst}$。我们的任务是：
1) 给每个 $a \in A$ 分配一个字符串标签 $l_a = {0, 1, *}^n$，其中比特宽度为 $n$，其中 $*$ 是通配符，可以匹配 0 和 1。2) 为每个 $p \in P$ 分配一个二进制字符串标签 $L_p = {0,1}^n$。3) 找到最小的 $n$，使得可以通过找到匹配 $L_p$ 的 $l_a \in \bigcup_{a.src = v}l_a$ 来正确转发具有路径 $p \in P$ 的数据包。

我们现在来描述如何将这个过程建模成一个SAT问题。对于每一个$a\in A$，它的标签$l_a$可以被表示为${x_a^1, x_a^2, \dots, x_a^n}$，其中$x_a^i\in{0,1,}$是边$a$的标签的第$i$个值。由于每个$x_a^i$有3个备选值，为了确定选择哪个值，我们需要使用两个布尔变量$u_a^i,v_a^i$来表示$x_a^i$的选择值。这里我们定义映射为$\overline{u}v=true$为$0$，$u\overline{v}=true$为$1$，$uv=true$为$*$。这个映射的优势在\cite{hsa}中有研究。对于每个 $p \in P$，$L_p$ 可以通过两个步骤轻松构建：
1）对于每个 $l_a \in \bigcup_{a \in p}l_a$ 的标签进行按位交集，结果表示为 $\hat{L_p}$，可能包含通配符；2）从与 $\hat{L_p}$ 匹配的有效位字符串中选择一个作为 $L_p$。

现在我们的目标是找到每个 $u_a^i, v_a^i, a \in A, 1 \le i \le n$ 的满足分配，同时使 $n$ 最小。为了构造子句，我们观察到必须满足两个限制条件。

\textbf{约束条件1}. 对于每个$p \in P$，所有$l_a \in \bigcup_{a \in p}l_a$的交集不能发生冲突。

\begin{equation}\small
C_1 = \bigwedge_{p \in P}\bigwedge\limits_{1 \le i \le n}(\bigwedge\limits_{a \in p} u_a^i \lor \bigwedge\limits_{a \in p} v_a^i)
\label{equ:c1}
\end{equation}

\textbf{约束条件2}. 对于每个具有超过2个出端口的节点$v \in V$，表示为$v.outs$，每对出端口标签都不能重叠。

\begin{equation}\small
C_2 = \bigwedge_{v \in V}\bigwedge_{a,b \in v.outs, a \neq b}\lnot \bigwedge\limits_{1 \le i \le n}(u_a^i \land u_b^i) \lor (v_a^i \land v_b^i)
\label{equ:c2}
\end{equation}

因此，有效路径编码的存在取决于是否存在满足分别为式（\ref{equ:c1}）和式（\ref{equ:c2}）的布尔公式的可满足解，这是一个可满足性问题（SAT问题）。我们可以进行一些转换并发现公式（\ref{equ:c1}）是2-SAT，公式（\ref{equ:c2}）是$n$-SAT，其中$n$是标签的位宽。因此，公式（\ref{equ:c3}）是$n$-SAT问题，当$n\geq 3$时是NP完全的。综合上述两个约束条件，最终目标的公式表示如式（\ref{equ:goal}）。
\begin{equation}\small
  \label{equ:goal}
      min\ n,\ 
      s.t.\ 
      C_3 = 1
  \end{equation}